Section: New Results

Proofs of Imperative Programs

• The Why3 reimplementation of the Why platform, started in 2010, was publicly released in 2011 [35] . The main developers are A. Paskevich, J.-C. Filliâtre, F. Bobot, and C. Marché. The language of Why, both programming and annotation parts, was significantly extended: algebraic types, records, pattern matching, recursive logical definitions are now supported. These logical declarations are structured in modules (a.k.a. theories). The module language comes with an original mechanism for reusing theories in specialized contexts using partial instantiations. These new features have been presented at the first international workshop on intermediate verification languages (BOOGIE 2011) [21] and will be presented at VSTTE 2012  [69] .

• A. Tafat and C. Marché used the Why3 system to perform a complete proof of the “Binary Heaps” challenge [41] from the VACID-0 international collection  [76] . Solving this challenge is a case study for a general approach of abstract interfaces for C programs, currently under development by A. Tafat, based on initial ideas described together with S. Boulmé which were published in a 2011 in a special issue [29] .

• In 2011, we set up a web gallery to publicly expose the programs that we specified and proved. This is the so-called ProVal collection of verified programs, and available at URL http://proval.lri.fr/gallery/index.en.html .

• K. Krishnamani and C. Marché proposed a technique for automatically generating loop invariants in C programs. It is based on the well-known predicate abstraction approach, which is adapted to take into account pre-existing specifications, and to proceed modularly, that is each function of a program is processed independently, with its own sets of predicates. The approach is also extended in order to generate universally quantified invariants [38] . The prototype is available as a Frama-C plugin at URL http://proval.lri.fr/agen .

• C. Dross, together with Y. Moy (Adacore) and J.-C. Filliâtre, addressed the problem of verifying programs involving containers. Containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. C. Dross gave a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and user-provided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. It relies on a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. C. Dross proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct. This work was presented at TAP 2011 [26] .

• Proving that pointer programs preserve data invariants, in a modular way, is known to be a challenge. R. Bardou and C. Marché designed a new approach based on advanced static typing systems (based on memory regions and permissions) to control memory updates and ownership of data [11] . A prototype implementation is built, called Capucine, available for download at http://romain.bardou.fr/capucine . To demonstrate the ability of this approach, the challenge “sparse arrays” of the VACID-0 benchmarks  [76] has been certified [30] .

• Separation logic has shown to be an elegant way to deal with programs which use data-structures with pointers. However it requires a specific logical language, provers, and specific reasoning techniques. In his PhD. F. Bobot introduced a technique to express ideas from separation logic in the traditional framework of deductive verification [12] . He proposed to derive “separation predicates” from user-supplied inductive definitions. These predicates come with suitable axiomatization, including frame rules, expressed in usual first-order logic. This translation takes special care to ensure the best use of automated theorem provers.